Speagram - Symbolic data analysis in Speagram

This part

…

This part

…

This part

…

This part

…

This part

…

This part

…

After we looked at search features of Speagram let us proceed to the most powerful part
of symbolic analysis methods present in Speagram - the possibility to use logic.

Speagram was built from scratch with the intention to make it possible to meaningfully
support automated reasoning and the use of logic. Even though our implementation of some
parts of the logic engine is at very early stages, we are quite convinced that the design
that we have chosen is right.

Before we describe how logic can be used in Speagram let us tell how the general design
of the logic part of Speagram is done and why we find it promising.
First of all, one of the main problems when reasoning about functional programs in the use
of mathematical induction. Many automated deduction systems start just with deduction and
try to add mathematical induction on top of it. While this is possible in theory, it tends
not to work too well in practice.

In Speagram we start with typed terms as basic object, so simple mathematical induction
is in a way built-in. Then we use a version of determinisation algorithm for tree automata
to cope with inductive reasoning. Only at this point we modify this algorithm so that it
works on formulas and does not explicitly use the automata, so it can be combined
with deductive methods. This together with basic simplification built into rewriting engine
allows us to have quite efficient logic support. In this way we can handle all formulas
where only tree-automatic function are used and even more when deduction or
a previously proved lemma is used to simplify the non-automatic part.

This part

…

Before we go on to the examples let us introduce the syntax of logic formulas in Speagram.
The formulas are constructed from equalities on normal Speagram terms,  boolean connectives
and quantifiers. The full syntax (built into Speagram) is as follows.
%P
Element ?a ''='' ?a as logic formula.
Element ''not'' logic formula as logic formula.
Element logic formula ''and'' logic formula as logic formula.
Element logic formula ''or'' logic formula as logic formula.
Element ''exists'' ?a '':'' logic formula as logic formula.
Element ''for'' ''all'' ?a '':'' logic formula as logic formula.
P%

Inside Speagram you will normally use formulas in three situations:
as axioms to add new axioms to Speagram, for searching (as shown above)
and to define and compute new relations.

By default Speagram tries to understand the relation you throw at it,
so it tries to construct a function that computes this relation.
We are going to see more complex example below, let us now just introduce the syntax.
%$
Load state library:/core.

New variable b as boolean.
Relation ''is'' boolean ''true?'' given by b = true.
Is false true?.
$%

This part

…

Basic relations on finite types are nice but not too useful.
Speagram can handle relations on infitite types.
Let us realize our promise and show how Speagram can automatically generate functions.
We are going to define binary numbers and the %P+P% function and then let Speagram
automatically construct the %P<=P% relation. Here comes the %P+P% on binary numbers. 
%$
Load state library:/core.

New class ''binary number''.
New element ''0'' as binary number.
New element ''1'' as binary number.
New element binary number ''0'' as binary number.
New element binary number ''1'' as binary number.

New variable n as binary number.
New variable m as binary number.
New variable k as binary number.

New function binary number ''+'' binary number as binary number.
See (n+(m0)) preferred to (n+m)0.
See (n+(m1)) preferred to (n+m)1.
See ((n+m)+k) preferred to (n+(m+k)).
Let 0 + n be n.
Let n + 0 be n.
Let 1 + 1 be 10.
Let n0 + 1 be n1.
Let n1 + 1 be (n+1)0.
Let 1 + n0 be n1.
Let 1 + n1 be (n+1)0.
Let n0 + m0 be (n+m)0.
Let n0 + m1 be (n+m)1.
Let n1 + m0 be (n+m)1.
Let n1 + m1 be (n+1+m)0.

This part

…

This part

…

This part

…